es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E. f2f+-pred(e',e)  (e' < e) 

latex

Definitions	f2f+-pred(e',e), e c e', [e: i p j], (e < e'), t.1, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), x:A.B(x), False, FIFO, ES, b, S  T, F2F+-decls, <a, b>, @i(x:T), , ff.R, Dec(P), P  Q, f(a), ff.S, Type, Id, s = t, loc(e), E, ff.C, x:AB(x), A, P & Q, , x:A  B(x), [e: i p j], x:A. B(x), Top, t  T, P  Q, left + right, x:A. B(x), let x,y = A in B(x;y), SQType(T), {T}, s ~ t, A c B, ff.Sender
Lemmas	es-causl transitivity2, fifoSender-causes, es-causl wf, top wf, snd-it wf, not wf, es-loc wf, fifoS wf, decidable wf, fifoR wf, es-dtype wf, bool wf, es-E wf, Id wf, fifoC wf, f2f+-pred wf, event system wf, FIFO wf, F2F+-decls wf